YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { add(0(), x) -> x
  , add(s(x), y) -> s(add(x, y))
  , mult(0(), x) -> 0()
  , mult(s(x), y) -> add(y, mult(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { mult(s(x), y) -> add(y, mult(x, y)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
   [add](x1, x2) = x1 + x2            
                                      
           [0]() = 0                  
                                      
         [s](x1) = 1 + x1             
                                      
  [mult](x1, x2) = 2*x1 + x1*x2 + 2*x2
                                      
  
  This order satisfies the following ordering constraints.
  
      [add(0(), x)] =  x                   
                    >= x                   
                    =  [x]                 
                                           
     [add(s(x), y)] =  1 + x + y           
                    >= 1 + x + y           
                    =  [s(add(x, y))]      
                                           
     [mult(0(), x)] =  2*x                 
                    >=                     
                    =  [0()]               
                                           
    [mult(s(x), y)] =  2 + 2*x + 3*y + x*y 
                    >  3*y + 2*x + x*y     
                    =  [add(y, mult(x, y))]
                                           

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { add(0(), x) -> x
  , add(s(x), y) -> s(add(x, y))
  , mult(0(), x) -> 0() }
Weak Trs: { mult(s(x), y) -> add(y, mult(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { add(s(x), y) -> s(add(x, y)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
   [add](x1, x2) = 2*x1 + x2          
                                      
           [0]() = 0                  
                                      
         [s](x1) = 2 + x1             
                                      
  [mult](x1, x2) = 2*x1 + x1*x2 + 2*x2
                                      
  
  This order satisfies the following ordering constraints.
  
      [add(0(), x)] =  x                   
                    >= x                   
                    =  [x]                 
                                           
     [add(s(x), y)] =  4 + 2*x + y         
                    >  2 + 2*x + y         
                    =  [s(add(x, y))]      
                                           
     [mult(0(), x)] =  2*x                 
                    >=                     
                    =  [0()]               
                                           
    [mult(s(x), y)] =  4 + 2*x + 4*y + x*y 
                    >  4*y + 2*x + x*y     
                    =  [add(y, mult(x, y))]
                                           

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { add(0(), x) -> x
  , mult(0(), x) -> 0() }
Weak Trs:
  { add(s(x), y) -> s(add(x, y))
  , mult(s(x), y) -> add(y, mult(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { add(0(), x) -> x }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
   [add](x1, x2) = 3 + x1 + x2             
                                           
           [0]() = 0                       
                                           
         [s](x1) = 1 + x1                  
                                           
  [mult](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2
                                           
  
  This order satisfies the following ordering constraints.
  
      [add(0(), x)] =  3 + x                      
                    >  x                          
                    =  [x]                        
                                                  
     [add(s(x), y)] =  4 + x + y                  
                    >= 4 + x + y                  
                    =  [s(add(x, y))]             
                                                  
     [mult(0(), x)] =  x                          
                    >=                            
                    =  [0()]                      
                                                  
    [mult(s(x), y)] =  3 + 5*x + 2*y + x*y + 2*x^2
                    >= 3 + 2*y + x + x*y + 2*x^2  
                    =  [add(y, mult(x, y))]       
                                                  

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs: { mult(0(), x) -> 0() }
Weak Trs:
  { add(0(), x) -> x
  , add(s(x), y) -> s(add(x, y))
  , mult(s(x), y) -> add(y, mult(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { mult(0(), x) -> 0() }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
   [add](x1, x2) = x1 + x2              
                                        
           [0]() = 0                    
                                        
         [s](x1) = 1 + x1               
                                        
  [mult](x1, x2) = 1 + x1 + 2*x1*x2 + x2
                                        
  
  This order satisfies the following ordering constraints.
  
      [add(0(), x)] =  x                   
                    >= x                   
                    =  [x]                 
                                           
     [add(s(x), y)] =  1 + x + y           
                    >= 1 + x + y           
                    =  [s(add(x, y))]      
                                           
     [mult(0(), x)] =  1 + x               
                    >                      
                    =  [0()]               
                                           
    [mult(s(x), y)] =  2 + x + 3*y + 2*x*y 
                    >  2*y + 1 + x + 2*x*y 
                    =  [add(y, mult(x, y))]
                                           

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { add(0(), x) -> x
  , add(s(x), y) -> s(add(x, y))
  , mult(0(), x) -> 0()
  , mult(s(x), y) -> add(y, mult(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^2))